SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Boolean satisfiability problem</title>

</head>

Boolean satisfiability problem

</h1>

</header>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hatnote{font-style:italic}.mw-parser-output div.hatnote{padding-left:1.6em;margin-bottom:0.5em}.mw-parser-output .hatnote i{font-style:normal}.mw-parser-output .hatnote+link+.hatnote{margin-top:-0.5em}@media print{body.ns-0 .mw-parser-output .hatnote{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div role="note" class="hatnote navigation-not-searchable">"3SAT" redirects here. For the Central European television network, see <a href="3sat" title="3sat">3sat</a>.</div>

In <a href="Logic" title="Logic">logic</a> and <a href="Computer_science" title="Computer science">computer science</a>, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) asks whether there exists an <a href="Interpretation_(logic)" title="Interpretation (logic)">interpretation</a> that <a href="Satisfiability" title="Satisfiability">satisfies</a> a given <a href="Boolean_logic" class="mw-redirect" title="Boolean logic">Boolean</a> <a href="Formula_(mathematical_logic)" class="mw-redirect" title="Formula (mathematical logic)">formula</a>. In other words, it asks whether the formula's variables can be consistently replaced by the values TRUE or FALSE to make the formula evaluate to TRUE. If this is the case, the formula is called satisfiable, else unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable.

SAT is the first problem that was proven to be <a href="NP-complete" class="mw-redirect" title="NP-complete">NP-complete</a>—this is the <a href="Cook%E2%80%93Levin_theorem" title="Cook–Levin theorem">Cook–Levin theorem</a>. This means that all problems in the complexity class <a href="NP_(complexity)" title="NP (complexity)">NP</a>, which includes a wide range of natural decision and optimization problems, are at most as difficult to solve as SAT. There is no known algorithm that efficiently solves each SAT problem (where "efficiently" means "deterministically in <a href="Time_complexity#Polynomial_time" title="Time complexity">polynomial time</a>"). Although such an algorithm is generally believed not to exist, this belief has not been proven or disproven mathematically. Resolving the question of whether SAT has a <a href="Polynomial-time" class="mw-redirect" title="Polynomial-time">polynomial-time</a> algorithm would settle the <a href="P_versus_NP_problem" title="P versus NP problem">P versus NP problem</a> - one of the most important open problems in the theory of computing.<a href="#cite_note-1">[1]</a><a href="#cite_note-2">[2]</a>

Nevertheless, as of 2007, heuristic SAT-algorithms are able to solve problem instances involving tens of thousands of variables and formulas consisting of millions of symbols,<a href="#cite_note-Codish.Ohrimenko.Stuckey.2007-3">[3]</a> which is sufficient for many practical SAT problems from, e.g., <a href="Artificial_intelligence" title="Artificial intelligence">artificial intelligence</a>, <a href="Circuit_design" title="Circuit design">circuit design</a>,<a href="#cite_note-4">[4]</a> and <a href="Automatic_theorem_proving" class="mw-redirect" title="Automatic theorem proving">automatic theorem proving</a>.

<div class="mw-heading mw-heading2"><h2 id="Definitions">Definitions</h2></div>

A <a href="Propositional_logic" title="Propositional logic">propositional logic</a> formula, also called Boolean expression, is built from <a href="Variable_(mathematics)" title="Variable (mathematics)">variables</a>, operators AND (<a href="Logical_conjunction" title="Logical conjunction">conjunction</a>, also denoted by ∧), OR (<a href="Logical_disjunction" title="Logical disjunction">disjunction</a>, ∨), NOT (<a href="Negation" title="Negation">negation</a>, ¬), and parentheses. A formula is said to be satisfiable if it can be made TRUE by assigning appropriate <a href="Logical_value" class="mw-redirect" title="Logical value">logical values</a> (i.e. TRUE, FALSE) to its variables. The Boolean satisfiability problem (SAT) is, given a formula, to check whether it is satisfiable. This <a href="Decision_problem" title="Decision problem">decision problem</a> is of central importance in many areas of <a href="Computer_science" title="Computer science">computer science</a>, including <a href="Theoretical_computer_science" title="Theoretical computer science">theoretical computer science</a>, <a href="Computational_complexity_theory" title="Computational complexity theory">complexity theory</a>,<a href="#cite_note-5">[5]</a><a href="#cite_note-6">[6]</a> <a href="Algorithmics" class="mw-redirect" title="Algorithmics">algorithmics</a>, <a href="Cryptography" title="Cryptography">cryptography</a><a href="#cite_note-7">[7]</a><a href="#cite_note-8">[8]</a> and <a href="Artificial_intelligence" title="Artificial intelligence">artificial intelligence</a>.<a href="#cite_note-9">[9]</a>

<div class="mw-heading mw-heading3"><h3 id="Conjunctive_normal_form">Conjunctive normal form</h3></div>

A literal is either a variable (in which case it is called a positive literal) or the negation of a variable (called a negative literal). A clause is a disjunction of literals (or a single literal). A clause is called a <a href="Horn_clause" title="Horn clause">Horn clause</a> if it contains at most one positive literal. A formula is in <a href="Conjunctive_normal_form" title="Conjunctive normal form">conjunctive normal form</a> (CNF) if it is a conjunction of clauses (or a single clause).

For example, x1 is a positive literal, ¬x2 is a negative literal, and x1 ∨ ¬x2 is a clause. The formula (x1 ∨ ¬x2) ∧ (¬x1 ∨ x2 ∨ x3) ∧ ¬x1 is in conjunctive normal form; its first and third clauses are Horn clauses, but its second clause is not. The formula is satisfiable, by choosing x1 = FALSE, x2 = FALSE, and x3 arbitrarily, since (FALSE ∨ ¬FALSE) ∧ (¬FALSE ∨ FALSE ∨ x3) ∧ ¬FALSE evaluates to (FALSE ∨ TRUE) ∧ (TRUE ∨ FALSE ∨ x3) ∧ TRUE, and in turn to TRUE ∧ TRUE ∧ TRUE (i.e. to TRUE). In contrast, the CNF formula a ∧ ¬a, consisting of two clauses of one literal, is unsatisfiable, since for a=TRUE or a=FALSE it evaluates to TRUE ∧ ¬TRUE (i.e., FALSE) or FALSE ∧ ¬FALSE (i.e., again FALSE), respectively.

For some versions of the SAT problem, it is useful to define the notion of a generalized conjunctive normal form formula, viz. as a conjunction of arbitrarily many generalized clauses, the latter being of the form R(l1,...,ln) for some <a href="Boolean_function" title="Boolean function">Boolean function</a> R and (ordinary) literals li. Different sets of allowed Boolean functions lead to different problem versions. As an example, R(¬x,a,b) is a generalized clause, and R(¬x,a,b) ∧ R(b,y,c) ∧ R(c,d,¬z) is a generalized conjunctive normal form. This formula is used <a href="#Exactly-1_3-satisfiability">below</a>, with R being the ternary operator that is TRUE just when exactly one of its arguments is.

Using the laws of <a href="Boolean_algebra_(structure)" title="Boolean algebra (structure)">Boolean algebra</a>, every propositional logic formula can be transformed into an equivalent conjunctive normal form, which may, however, be exponentially longer. For example, transforming the formula (x1∧y1) ∨ (x2∧y2) ∨ ... ∨ (xn∧yn) into conjunctive normal form yields

/* start https://en.wikipedia.org/ */

.mw-parser-output .block-indent{padding-left:3em;padding-right:0;overflow:hidden}

/* end https://en.wikipedia.org/ */

</style><div class="block-indent">(x1 ∨ x2 ∨ … ∨ xn) ∧</div>

while the former is a disjunction of n conjunctions of 2 variables, the latter consists of 2n clauses of n variables.

However, with use of the <a href="Tseytin_transformation" title="Tseytin transformation">Tseytin transformation</a>, we may find an equisatisfiable conjunctive normal form formula with length linear in the size of the original propositional logic formula.

<div class="mw-heading mw-heading2"><h2 id="Complexity">Complexity</h2></div>

<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Cook%E2%80%93Levin_theorem" title="Cook–Levin theorem">Cook–Levin theorem</a></div>

SAT was the first problem known to be <a href="NP-complete" class="mw-redirect" title="NP-complete">NP-complete</a>, as proved by <a href="Stephen_Cook" title="Stephen Cook">Stephen Cook</a> at the <a href="University_of_Toronto" title="University of Toronto">University of Toronto</a> in 1971<a href="#cite_note-10">[10]</a> and independently by <a href="Leonid_Levin" title="Leonid Levin">Leonid Levin</a> at the <a href="Russian_Academy_of_Sciences#The_Academy_of_Sciences_of_the_USSR" title="Russian Academy of Sciences">Russian Academy of Sciences</a> in 1973.<a href="#cite_note-11">[11]</a> Until that time, the concept of an NP-complete problem did not even exist. The proof shows how every decision problem in the <a href="Complexity_class" title="Complexity class">complexity class</a> <a href="NP_(complexity)" title="NP (complexity)">NP</a> can be <a href="Reduction_(complexity)" title="Reduction (complexity)">reduced</a> to the SAT problem for CNF<a href="#cite_note-12">[a]</a> formulas, sometimes called CNFSAT. A useful property of Cook's reduction is that it preserves the number of accepting answers. For example, deciding whether a given <a href="Graph_(discrete_mathematics)" title="Graph (discrete mathematics)">graph</a> has a <a href="Graph_coloring#Vertex_coloring" title="Graph coloring">3-coloring</a> is another problem in NP; if a graph has 17 valid 3-colorings, then the SAT formula produced by the Cook–Levin reduction will have 17 satisfying assignments.

NP-completeness only refers to the run-time of the worst case instances. Many of the instances that occur in practical applications can be solved much more quickly. See <a href="#Algorithms_for_solving_SAT">§Algorithms for solving SAT</a> below.

<div class="mw-heading mw-heading3"><h3 id="3-satisfiability">3-satisfiability</h3></div>

Like the satisfiability problem for arbitrary formulas, determining the satisfiability of a formula in conjunctive normal form where each clause is limited to at most three literals is NP-complete also; this problem is called 3-SAT, 3CNFSAT, or 3-satisfiability. To reduce the unrestricted SAT problem to 3-SAT, transform each clause l1 ∨ ⋯ ∨ ln to a conjunction of n - 2 clauses

where x2, ⋯ , xn−2 are <a href="Fresh_variable" title="Fresh variable">fresh variables</a> not occurring elsewhere. Although the two formulas are not <a href="Logically_equivalent" class="mw-redirect" title="Logically equivalent">logically equivalent</a>, they are <a href="Equisatisfiable" class="mw-redirect" title="Equisatisfiable">equisatisfiable</a>. The formula resulting from transforming all clauses is at most 3 times as long as its original; that is, the length growth is polynomial.<a href="#cite_note-FOOTNOTEAhoHopcroftUllman1974Theorem_10.4-13">[12]</a>

3-SAT is one of <a href="Karp's_21_NP-complete_problems" title="Karp's 21 NP-complete problems">Karp's 21 NP-complete problems</a>, and it is used as a starting point for proving that other problems are also <a href="NP-hard" class="mw-redirect" title="NP-hard">NP-hard</a>.<a href="#cite_note-14">[b]</a> This is done by <a href="Polynomial-time_reduction" title="Polynomial-time reduction">polynomial-time reduction</a> from 3-SAT to the other problem. An example of a problem where this method has been used is the <a href="Clique_problem" title="Clique problem">clique problem</a>: given a CNF formula consisting of c clauses, the corresponding <a href="Graph_(discrete_mathematics)" title="Graph (discrete mathematics)">graph</a> consists of a vertex for each literal, and an edge between each two non-contradicting<a href="#cite_note-15">[c]</a> literals from different clauses; see the picture. The graph has a c-clique if and only if the formula is satisfiable.<a href="#cite_note-FOOTNOTEAhoHopcroftUllman1974Theorem_10.5-16">[13]</a>

There is a simple randomized algorithm due to Schöning (1999) that runs in time (4/3)n where n is the number of variables in the 3-SAT proposition, and succeeds with high probability to correctly decide 3-SAT.<a href="#cite_note-Schoning.1999-17">[14]</a>

The <a href="Exponential_time_hypothesis" title="Exponential time hypothesis">exponential time hypothesis</a> asserts that no algorithm can solve 3-SAT (or indeed k-SAT for any k > 2) in exp(<a href="Small_o_notation" class="mw-redirect" title="Small o notation">o</a>(n)) time (that is, fundamentally faster than exponential in n).

Selman, Mitchell, and Levesque (1996) give empirical data on the difficulty of randomly generated 3-SAT formulas, depending on their size parameters. Difficulty is measured in number recursive calls made by a <a href="DPLL_algorithm" title="DPLL algorithm">DPLL algorithm</a>. They identified a phase transition region from almost-certainly-satisfiable to almost-certainly-unsatisfiable formulas at the clauses-to-variables ratio at about 4.26.<a href="#cite_note-18">[15]</a>

3-satisfiability can be generalized to k-satisfiability (k-SAT, also k-CNF-SAT), when formulas in CNF are considered with each clause containing up to k literals. However, since for any k ≥ 3, this problem can neither be easier than 3-SAT nor harder than SAT, and the latter two are NP-complete, so must be k-SAT.

Some authors restrict k-SAT to CNF formulas with exactly k literals. This does not lead to a different complexity class either, as each clause l1 ∨ ⋯ ∨ lj with j < k literals can be padded with fixed dummy variables to l1 ∨ ⋯ ∨ lj ∨ dj+1 ∨ ⋯ ∨ dk. After padding all clauses, 2k–1 extra clauses<a href="#cite_note-19">[d]</a> must be appended to ensure that only d1 = ⋯ = dk = FALSE can lead to a satisfying assignment. Since k does not depend on the formula length, the extra clauses lead to a constant increase in length. For the same reason, it does not matter whether duplicate literals are allowed in clauses, as in ¬x ∨ ¬y ∨ ¬y.

<div class="mw-heading mw-heading2"><h2 id="Special_instances_of_3SAT">Special instances of 3SAT</h2></div>

<div class="mw-heading mw-heading3"><h3 id="Conjunctive_normal_form_2">Conjunctive normal form</h3></div>

Conjunctive normal form (in particular with 3 literals per clause) is often considered the canonical representation for SAT formulas. As shown above, the general SAT problem reduces to 3-SAT, the problem of determining satisfiability for formulas in this form.

<div class="mw-heading mw-heading3"><h3 id="Linear_SAT">Linear SAT</h3></div>

A 3-SAT formula is Linear SAT (LSAT) if each clause (viewed as a set of literals) intersects at most one other clause, and, moreover, if two clauses intersect, then they have exactly one literal in common. An LSAT formula can be depicted as a set of disjoint semi-closed intervals on a line. Deciding whether an LSAT formula is satisfiable is NP-complete.<a href="#cite_note-20">[16]</a>

<div class="mw-heading mw-heading3"><h3 id="2-satisfiability">2-satisfiability</h3></div>

<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="2-satisfiability" title="2-satisfiability">2-satisfiability</a></div>

SAT is easier if the number of literals in a clause is limited to at most 2, in which case the problem is called <a href="2-satisfiability" title="2-satisfiability">2-SAT</a>. This problem can be solved in polynomial time, and in fact is <a href="NL-complete" title="NL-complete">complete</a> for the complexity class <a href="NL_(complexity)" title="NL (complexity)">NL</a>. If additionally all OR operations in literals are changed to <a href="Exclusive_or" title="Exclusive or">XOR</a> operations, then the result is called exclusive-or 2-satisfiability, which is a problem complete for the complexity class <a href="SL_(complexity)" title="SL (complexity)">SL</a> = <a href="L_(complexity)" title="L (complexity)">L</a>.

<div class="mw-heading mw-heading3"><h3 id="Horn-satisfiability">Horn-satisfiability</h3></div>

<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Horn-satisfiability" title="Horn-satisfiability">Horn-satisfiability</a></div>

The problem of deciding the satisfiability of a given conjunction of <a href="Horn_clause" title="Horn clause">Horn clauses</a> is called Horn-satisfiability, or HORN-SAT. It can be solved in polynomial time by a single step of the <a href="Unit_propagation" title="Unit propagation">unit propagation</a> algorithm, which produces the single minimal model of the set of Horn clauses (w.r.t. the set of literals assigned to TRUE). Horn-satisfiability is <a href="P-complete" title="P-complete">P-complete</a>. It can be seen as <a href="P_(complexity)" title="P (complexity)">P's</a> version of the Boolean satisfiability problem. Also, deciding the truth of quantified Horn formulas can be done in polynomial time.<a href="#cite_note-buningkarpinski-21">[17]</a>

Horn clauses are of interest because they are able to express <a href="Entailment" class="mw-redirect" title="Entailment">implication</a> of one variable from a set of other variables. Indeed, one such clause ¬x1 ∨ ... ∨ ¬xn ∨ y can be rewritten as x1 ∧ ... ∧ xn → y; that is, if x1,...,xn are all TRUE, then y must be TRUE as well.

A generalization of the class of Horn formulas is that of renameable-Horn formulae, which is the set of formulas that can be placed in Horn form by replacing some variables with their respective negation. For example, (x1 ∨ ¬x2) ∧ (¬x1 ∨ x2 ∨ x3) ∧ ¬x1 is not a Horn formula, but can be renamed to the Horn formula (x1 ∨ ¬x2) ∧ (¬x1 ∨ x2 ∨ ¬y3) ∧ ¬x1 by introducing y3 as negation of x3. In contrast, no renaming of (x1 ∨ ¬x2 ∨ ¬x3) ∧ (¬x1 ∨ x2 ∨ x3) ∧ ¬x1 leads to a Horn formula. Checking the existence of such a replacement can be done in linear time; therefore, the satisfiability of such formulae is in P as it can be solved by first performing this replacement and then checking the satisfiability of the resulting Horn formula.

<div class="mw-heading mw-heading2"><h2 id="Not_3SAT_problems">Not 3SAT problems</h2></div>

<div class="mw-heading mw-heading3"><h3 id="Disjunctive_normal_form">Disjunctive normal form</h3></div>

SAT is trivial if the formulas are restricted to those in <a href="Disjunctive_normal_form" title="Disjunctive normal form">disjunctive normal form</a>, that is, they are a disjunction of conjunctions of literals. Such a formula is indeed satisfiable if and only if at least one of its conjunctions is satisfiable, and a conjunction is satisfiable if and only if it does not contain both x and NOT x for some variable x. This can be checked in linear time. Furthermore, if they are restricted to being in full disjunctive normal form, in which every variable appears exactly once in every conjunction, they can be checked in constant time (each conjunction represents one satisfying assignment). But it can take exponential time and space to convert a general SAT problem to disjunctive normal form; to obtain an example, exchange "∧" and "∨" in the <a href="#Definitions">above</a> exponential blow-up example for conjunctive normal forms.

<div class="mw-heading mw-heading3"><h3 id="Exactly-1_3-satisfiability">Exactly-1 3-satisfiability</h3></div>

<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="1-in-3-SAT" title="1-in-3-SAT">1-in-3-SAT</a></div>

Another NP-complete variant of the 3-satisfiability problem is the one-in-three 3-SAT (also known variously as 1-in-3-SAT and exactly-1 3-SAT). Given a conjunctive normal form with three literals per clause, the problem is to determine whether there exists a truth assignment to the variables so that each clause has exactly one TRUE literal (and thus exactly two FALSE literals).

<div class="mw-heading mw-heading3"><h3 id="Not-all-equal_3-satisfiability">Not-all-equal 3-satisfiability</h3></div>

<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Not-all-equal_3-satisfiability" title="Not-all-equal 3-satisfiability">Not-all-equal 3-satisfiability</a></div>

Another variant is the not-all-equal 3-satisfiability problem (also called NAE3SAT). Given a conjunctive normal form with three literals per clause, the problem is to determine if an assignment to the variables exists such that in no clause all three literals have the same truth value. This problem is NP-complete, too, even if no negation symbols are admitted, by Schaefer's dichotomy theorem.<a href="#cite_note-schaefer-22">[18]</a>

<div class="mw-heading mw-heading3"><h3 id="XOR-satisfiability">XOR-satisfiability</h3></div>

<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="XOR-SAT" title="XOR-SAT">XOR-SAT</a></div>

Another special case is the class of problems where each clause contains XOR (i.e. <a href="Exclusive_or" title="Exclusive or">exclusive or</a>) rather than (plain) OR operators. This is in <a href="P_(complexity_class)" class="mw-redirect" title="P (complexity class)">P</a>, since an XOR-SAT formula can also be viewed as a system of linear equations mod 2, and can be solved in cubic time by <a href="Gaussian_elimination" title="Gaussian elimination">Gaussian elimination</a>;<a href="#cite_note-23">[19]</a>

<div class="mw-heading mw-heading2"><h2 id="Schaefer's_dichotomy_theorem">Schaefer's dichotomy theorem</h2></div>

<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Schaefer's_dichotomy_theorem" title="Schaefer's dichotomy theorem">Schaefer's dichotomy theorem</a></div>

The restrictions above (CNF, 2CNF, 3CNF, Horn, XOR-SAT) bound the considered formulae to be conjunctions of subformulas; each restriction states a specific form for all subformulas: for example, only binary clauses can be subformulas in 2CNF.

Schaefer's dichotomy theorem states that, for any restriction to Boolean functions that can be used to form these subformulas, the corresponding satisfiability problem is in P or NP-complete. The membership in P of the satisfiability of 2CNF, Horn, and XOR-SAT formulae are special cases of this theorem.<a href="#cite_note-schaefer-22">[18]</a>

The following table summarizes some common variants of SAT.

</caption>

<th>Name

</th>

<th>Code

</th>

<th>3SAT problem?

</th>

<th>Restrictions

</th>

<th>Requirements

</th>

<th>Class

</th></tr>

<tr>

<td>3-satisfiability

</td>

</td>

<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes

</td>

<td>Each clause contains 3 literals.

</td>

<td>At least one literal must be true.

</td>

<td>NP-c

</td></tr>

<tr>

<td>2-satisfiability

</td>

</td>

<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes

</td>

<td>Each clause contains 2 literals.

</td>

<td>At least one literal must be true.

</td>

<td>NL-c

</td></tr>

<tr>

<td>Exactly-1 3-SAT

</td>

</td>

<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No

</td>

<td>Each clause contains 3 literals.

</td>

<td>Exactly one literal must be true.

</td>

<td>NP-c

</td></tr>

<tr>

<td>Exactly-1 Positive 3-SAT

</td>

</td>

<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No

</td>

<td>Each clause contains 3 positive literals.

</td>

<td>Exactly one literal must be true.

</td>

<td>NP-c

</td></tr>

<tr>

<td>Not-all-equal 3-satisfiability

</td>

</td>

<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No

</td>

<td>Each clause contains 3 literals.

</td>

<td>Either one or two literals must be true.

</td>

<td>NP-c

</td></tr>

<tr>

<td>Not-all-equal positive 3-SAT

</td>

</td>

<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No

</td>

<td>Each clause contains 3 positive literals.

</td>

<td>Either one or two literals must be true.

</td>

<td>NP-c

</td></tr>

<tr>

<td><a href="Planar_SAT" title="Planar SAT">Planar SAT</a>

</td>

</td>

<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes

</td>

<td>The incidence graph (clause-variable graph) is <a href="Planar_graph" title="Planar graph">planar</a>.

</td>

<td>At least one literal must be true.

</td>

<td>NP-c

</td></tr>

<tr>

<td>Linear SAT

</td>

</td>

<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes

</td>

<td>Each clause contains 3 literals, intersects at most one other clause, and the intersection is exactly one literal.

</td>

<td>At least one literal must be true.

</td>

<td>NP-c

</td></tr>

<tr>

<td>Horn satisfiability

</td>

</td>

<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes

</td>

<td>Horn clauses (at most one positive literal).

</td>

<td>At least one literal must be true.

</td>

<td>P-c

</td></tr>

<tr>

<td>Xor satisfiability

</td>

</td>

<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No

</td>

<td>Each clause contains XOR operations rather than OR.

</td>

<td>The XOR of all literals must be true.

</td>

<td>P

</td></tr></tbody></table>

<div class="mw-heading mw-heading2"><h2 id="Extensions_of_SAT">Extensions of SAT</h2></div>

An extension that has gained significant popularity since 2003 is <a href="Satisfiability_modulo_theories" title="Satisfiability modulo theories">satisfiability modulo theories</a> (SMT) that can enrich CNF formulas with linear constraints, arrays, all-different constraints, <a href="Uninterpreted_function" title="Uninterpreted function">uninterpreted functions</a>,<a href="#cite_note-Bryant.German.Velev.1999-24">[20]</a> etc. Such extensions typically remain NP-complete, but very efficient solvers are now available that can handle many such kinds of constraints.

The satisfiability problem becomes more difficult if both "for all" (<a href="%E2%88%80" class="mw-redirect" title="∀">∀</a>) and "there exists" (<a href="%E2%88%83" class="mw-redirect" title="∃">∃</a>) <a href="Quantifier_(logic)" title="Quantifier (logic)">quantifiers</a> are allowed to bind the Boolean variables. An example of such an expression would be ∀x ∀y ∃z (x ∨ y ∨ z) ∧ (¬x ∨ ¬y ∨ ¬z); it is valid, since for all values of x and y, an appropriate value of z can be found, viz. z=TRUE if both x and y are FALSE, and z=FALSE else. SAT itself (tacitly) uses only ∃ quantifiers. If only ∀ quantifiers are allowed instead, the so-called <a href="Tautology_(logic)" title="Tautology (logic)">tautology</a> problem is obtained, which is <a href="Co-NP-complete" title="Co-NP-complete">co-NP-complete</a>. If any number of both quantifiers are allowed, the problem is called the <a href="Quantified_Boolean_formula_problem" class="mw-redirect" title="Quantified Boolean formula problem">quantified Boolean formula problem</a> (QBF), which can be shown to be <a href="PSPACE-complete" title="PSPACE-complete">PSPACE-complete</a>. It is widely believed that PSPACE-complete problems are strictly harder than any problem in NP, although this has not yet been proved.

Ordinary SAT asks if there is at least one variable assignment that makes the formula true. A variety of variants deal with the number of such assignments:

<ul><li>MAJ-SAT asks if at least half of all assignments make the formula TRUE. It is known to be complete for <a href="PP_(complexity)" title="PP (complexity)">PP</a>, a probabilistic class. Surprisingly, MAJ-kSAT is demonstrated to be in P for every finite integer k.<a href="#cite_note-25">[21]</a></li>

<li><a href="Sharp-SAT" title="Sharp-SAT">#SAT</a>, the problem of counting how many variable assignments satisfy a formula, is a counting problem, not a decision problem, and is <a href="Sharp-P-complete" class="mw-redirect" title="Sharp-P-complete">#P-complete</a>.</li>

<li>UNIQUE SAT<a href="#cite_note-26">[22]</a> is the problem of determining whether a formula has exactly one assignment. It is complete for US,<a href="#cite_note-27">[23]</a> the <a href="Complexity_class" title="Complexity class">complexity class</a> describing problems solvable by a non-deterministic polynomial time <a href="Turing_machine" title="Turing machine">Turing machine</a> that accepts when there is exactly one nondeterministic accepting path and rejects otherwise.</li>

<li>UNAMBIGUOUS-SAT is the name given to the satisfiability problem when the input formula is <a href="Promise_problem" title="Promise problem">promised</a> to have at most one satisfying assignment. The problem is also called USAT.<a href="#cite_note-28">[24]</a> A solving algorithm for UNAMBIGUOUS-SAT is allowed to exhibit any behavior, including endless looping, on a formula having several satisfying assignments. Although this problem seems easier, Valiant and Vazirani have <a href="Valiant%E2%80%93Vazirani_theorem" title="Valiant–Vazirani theorem">shown</a><a href="#cite_note-29">[25]</a> that if there is a practical (i.e. <a href="Bounded-error_probabilistic_polynomial" class="mw-redirect" title="Bounded-error probabilistic polynomial">randomized polynomial-time</a>) algorithm to solve it, then all problems in <a href="NP_(complexity_class)" class="mw-redirect" title="NP (complexity class)">NP</a> can be solved just as easily.</li>

<li>MAX-SAT, the <a href="Maximum_satisfiability_problem" title="Maximum satisfiability problem">maximum satisfiability problem</a>, is an <a href="FNP_(complexity)" title="FNP (complexity)">FNP</a> generalization of SAT. It asks for the maximum number of clauses which can be satisfied by any assignment. It has efficient <a href="Approximation_algorithm" title="Approximation algorithm">approximation algorithms</a>, but is NP-hard to solve exactly. Worse still, it is <a href="APX" title="APX">APX</a>-complete, meaning there is no <a href="Polynomial-time_approximation_scheme" title="Polynomial-time approximation scheme">polynomial-time approximation scheme</a> (PTAS) for this problem unless P=NP.</li>

<li>WMSAT is the problem of finding an assignment of minimum weight that satisfy a monotone Boolean formula (i.e. a formula without any negation). Weights of propositional variables are given in the input of the problem. The weight of an assignment is the sum of weights of true variables. That problem is NP-complete (see Th. 1 of <a href="#cite_note-30">[26]</a>).</li></ul>

Other generalizations include satisfiability for <a href="First-order_predicate_calculus" class="mw-redirect" title="First-order predicate calculus">first</a>- and <a href="Second-order_logic" title="Second-order logic">second-order logic</a>, <a href="Constraint_satisfaction_problem" title="Constraint satisfaction problem">constraint satisfaction problems</a>, <a href="0-1_integer_programming" class="mw-redirect" title="0-1 integer programming">0-1 integer programming</a>.

<div class="mw-heading mw-heading2"><h2 id="Finding_a_satisfying_assignment">Finding a satisfying assignment</h2></div>

While SAT is a <a href="Decision_problem" title="Decision problem">decision problem</a>, the <a href="Search_problem" title="Search problem">search problem</a> of finding a satisfying assignment reduces to SAT. That is, each algorithm which correctly answers whether an instance of SAT is solvable can be used to find a satisfying assignment. First, the question is asked on the given formula Φ. If the answer is "no", the formula is unsatisfiable. Otherwise, the question is asked on the partly instantiated formula Φ<a href="Substitution_(logic)" title="Substitution (logic)">{x1=TRUE}</a>, that is, Φ with the first variable x1 replaced by TRUE, and simplified accordingly. If the answer is "yes", then x1=TRUE, otherwise x1=FALSE. Values of other variables can be found subsequently in the same way. In total, n+1 runs of the algorithm are required, where n is the number of distinct variables in Φ.

This property is used in several theorems in complexity theory:

<ul><li><a href="NP_(complexity)" title="NP (complexity)">NP</a> ⊆ <a href="P/poly" title="P/poly">P/poly</a> ⇒ <a href="PH_(complexity)" class="mw-redirect" title="PH (complexity)">PH</a> = <a href="Polynomial_hierarchy#Definitions" title="Polynomial hierarchy">Σ2</a> (<a href="Karp%E2%80%93Lipton_theorem" title="Karp–Lipton theorem">Karp–Lipton theorem</a>)</li>

<div class="mw-heading mw-heading2"><h2 id="Algorithms_for_solving_SAT">Algorithms for solving SAT</h2></div>

<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="SAT_solver" title="SAT solver">SAT solver</a></div>

Since the SAT problem is NP-complete, only algorithms with exponential worst-case complexity are known for it. In spite of this, efficient and scalable algorithms for SAT were developed during the 2000s and have contributed to dramatic advances in the ability to automatically solve problem instances involving tens of thousands of variables and millions of constraints (i.e. clauses).<a href="#cite_note-Codish.Ohrimenko.Stuckey.2007-3">[3]</a> Examples of such problems in <a href="Electronic_design_automation" title="Electronic design automation">electronic design automation</a> (EDA) include <a href="Formal_equivalence_checking" title="Formal equivalence checking">formal equivalence checking</a>, <a href="Model_checking" title="Model checking">model checking</a>, <a href="Formal_verification" title="Formal verification">formal verification</a> of <a href="Microprocessor" title="Microprocessor">pipelined microprocessors</a>,<a href="#cite_note-Bryant.German.Velev.1999-24">[20]</a> <a href="Automatic_test_pattern_generation" title="Automatic test pattern generation">automatic test pattern generation</a>, <a href="Routing_(electronic_design_automation)" title="Routing (electronic design automation)">routing</a> of <a href="FPGA" class="mw-redirect" title="FPGA">FPGAs</a>,<a href="#cite_note-31">[27]</a> <a href="Automated_planning_and_scheduling" title="Automated planning and scheduling">planning</a>, and <a href="Scheduling_algorithm" class="mw-redirect" title="Scheduling algorithm">scheduling problems</a>, and so on. A SAT-solving engine is also considered to be an essential component in the <a href="Electronic_design_automation" title="Electronic design automation">electronic design automation</a> toolbox.

Major techniques used by modern SAT solvers include the <a href="Davis%E2%80%93Putnam%E2%80%93Logemann%E2%80%93Loveland_algorithm" class="mw-redirect" title="Davis–Putnam–Logemann–Loveland algorithm">Davis–Putnam–Logemann–Loveland algorithm</a> (or DPLL), <a href="Conflict-driven_clause_learning" title="Conflict-driven clause learning">conflict-driven clause learning</a> (CDCL), and <a href="Stochastic" title="Stochastic">stochastic</a> <a href="Local_search_(constraint_satisfaction)" title="Local search (constraint satisfaction)">local search</a> algorithms such as <a href="WalkSAT" title="WalkSAT">WalkSAT</a>. Almost all SAT solvers include time-outs, so they will terminate in reasonable time even if they cannot find a solution. Different SAT solvers will find different instances easy or hard, and some excel at proving unsatisfiability, and others at finding solutions. Recent attempts have been made to learn an instance's satisfiability using deep learning techniques.<a href="#cite_note-32">[28]</a>

SAT solvers are developed and compared in SAT-solving contests.<a href="#cite_note-33">[29]</a> Modern SAT solvers are also having significant impact on the fields of software verification, constraint solving in artificial intelligence, and <a href="Operations_research" title="Operations research">operations research</a>, among others.

<ul><li><a href="Unsatisfiable_core" title="Unsatisfiable core">Unsatisfiable core</a></li>

<li><a href="Satisfiability_modulo_theories" title="Satisfiability modulo theories">Satisfiability modulo theories</a></li>

<li><a href="Sharp-SAT" title="Sharp-SAT">Counting SAT</a></li>

<li><a href="Planar_SAT" title="Planar SAT">Planar SAT</a></li>

<li><a href="Karloff%E2%80%93Zwick_algorithm" title="Karloff–Zwick algorithm">Karloff–Zwick algorithm</a></li>

<li><a href="Circuit_satisfiability" class="mw-redirect" title="Circuit satisfiability">Circuit satisfiability</a></li></ul>

<div class="mw-heading mw-heading2"><h2 id="Notes">Notes</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist reflist-lower-alpha">

<li id="cite_note-12"><a href="#cite_ref-12">^</a> The SAT problem for arbitrary formulas is NP-complete, too, since it is easily shown to be in NP, and it cannot be easier than SAT for CNF formulas.

</li>

<li id="cite_note-14"><a href="#cite_ref-14">^</a> i.e. at least as hard as every other problem in NP. A decision problem is NP-complete if and only if it is in NP and is NP-hard.

</li>

<li id="cite_note-15"><a href="#cite_ref-15">^</a> i.e. such that one literal is not the negation of the other

</li>

<li id="cite_note-19"><a href="#cite_ref-19">^</a> viz. all <a href="Canonical_form_(Boolean_algebra)" class="mw-redirect" title="Canonical form (Boolean algebra)">maxterms</a> that can be built with d1,⋯,dk, except d1∨⋯∨dk

</li>

</ol></div></div>

<div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .side-box{margin:4px 0;box-sizing:border-box;border:1px solid #aaa;font-size:88%;line-height:1.25em;background-color:var(--background-color-interactive-subtle,#f8f9fa);display:flow-root}.mw-parser-output .infobox .side-box{font-size:100%}.mw-parser-output .side-box-abovebelow,.mw-parser-output .side-box-text{padding:0.25em 0.9em}.mw-parser-output .side-box-image{padding:2px 0 2px 0.9em;text-align:center}.mw-parser-output .side-box-imageright{padding:2px 0.9em 2px 0;text-align:center}@media(min-width:500px){.mw-parser-output .side-box-flex{display:flex;align-items:center}.mw-parser-output .side-box-text{flex:1;min-width:0}}@media(min-width:720px){.mw-parser-output .side-box{width:238px}.mw-parser-output .side-box-right{clear:right;float:right;margin-left:1em}.mw-parser-output .side-box-left{margin-right:1em}}

/* end https://en.wikipedia.org/ */

</style><style data-mw-deduplicate="TemplateStyles:r1237033735">

/* start https://en.wikipedia.org/ */

@media print{body.ns-0 .mw-parser-output .sistersitebox{display:none!important}}@media screen{html.skin-theme-clientpref-night .mw-parser-output .sistersitebox img[src*="Wiktionary-logo-en-v2.svg"]{background-color:white}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .sistersitebox img[src*="Wiktionary-logo-en-v2.svg"]{background-color:white}}

/* end https://en.wikipedia.org/ */

</style><div class="side-box side-box-right sistersitebox"><style data-mw-deduplicate="TemplateStyles:r1126788409">

/* start https://en.wikipedia.org/ */

.mw-parser-output .plainlist ol,.mw-parser-output .plainlist ul{line-height:inherit;list-style:none;margin:0;padding:0}.mw-parser-output .plainlist ol li,.mw-parser-output .plainlist ul li{margin-bottom:0}

/* end https://en.wikipedia.org/ */

</style>

<div class="side-box-text plainlist">Wikimedia Commons has media related to <a href="https://commons.wikimedia.org/wiki/Category:Boolean_satisfiability_problem" class="extiw external" title="commons:Category:Boolean satisfiability problem">Boolean satisfiability problem</a>.</div></div>

</div>

<ul><li><a rel="nofollow" class="external text" href="http://www.cril.univ-artois.fr/~roussel/satgame/satgame.php?lang=eng">SAT Game</a>: try solving a Boolean satisfiability problem yourself</li>

<li><a rel="nofollow" class="external text" href="http://www.satcompetition.org/">The international SAT competition website</a></li>

<li><a rel="nofollow" class="external text" href="http://www.satisfiability.org/">International Conference on Theory and Applications of Satisfiability Testing</a></li>

<li><a rel="nofollow" class="external text" href="https://web.archive.org/web/20060219180520/http://jsat.ewi.tudelft.nl/">Journal on Satisfiability, Boolean Modeling and Computation</a></li>

<li><a rel="nofollow" class="external text" href="http://www.satlive.org">SAT Live, an aggregate website for research on the satisfiability problem</a></li>

<li><a rel="nofollow" class="external text" href="http://www.maxsat.udl.cat/">Yearly evaluation of MaxSAT solvers</a></li></ul>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFFortnow,_L.2009" class="citation journal cs1">Fortnow, L. (2009). <a rel="nofollow" class="external text" href="https://www.cs.cmu.edu/~15326-f23/CACM-Fortnow.pdf">"The status of the P versus NP problem"</a> (PDF). Communications of the ACM. 52 (9): 78–86. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F1562164.1562186">10.1145/1562164.1562186</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:5969255">5969255</a>.</cite>

</li>

<li id="cite_note-2"><a href="#cite_ref-2">^</a> <cite id="CITEREFFortnow,_L.2021" class="citation journal cs1">Fortnow, L. (2021). <a rel="nofollow" class="external text" href="https://lance.fortnow.com/papers/files/pvnp50.pdf">"Fifty Years of P Versus NP and the Possibility of the Impossible"</a> (PDF). Proceedings of ACM Conference (Conference'17).</cite>

</li>

<li id="cite_note-Codish.Ohrimenko.Stuckey.2007-3">^ <a href="#cite_ref-Codish.Ohrimenko.Stuckey.2007_3-0">a</a> <a href="#cite_ref-Codish.Ohrimenko.Stuckey.2007_3-1">b</a> <cite id="CITEREFOhrimenkoStuckeyCodish2007" class="citation cs2">Ohrimenko, Olga; Stuckey, Peter J.; Codish, Michael (2007), "Propagation = Lazy Clause Generation", Principles and Practice of Constraint Programming – CP 2007, Lecture Notes in Computer Science, vol. 4741, pp. 544–558, <a href="CiteSeerX_(identifier)" class="mw-redirect" title="CiteSeerX (identifier)">CiteSeerX</a> <a rel="nofollow" class="external text" href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.70.5471">10.1.1.70.5471</a>, <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-540-74970-7_39">10.1007/978-3-540-74970-7_39</a>, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-540-74969-1</bdi>, <q>modern SAT solvers can often handle problems with millions of constraints and hundreds of thousands of variables</q></cite>.

</li>

<li id="cite_note-4"><a href="#cite_ref-4">^</a> <cite id="CITEREFHongLiParkMui2010" class="citation book cs1">Hong, Ted; Li, Yanjing; Park, Sung-Boem; Mui, Diana; Lin, David; Kaleq, Ziyad Abdel; Hakim, Nagib; Naeimi, Helia; Gardner, Donald S.; Mitra, Subhasish (November 2010). "QED: Quick Error Detection tests for effective post-silicon validation". 2010 IEEE International Test Conference. pp. 1–10. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FTEST.2010.5699215">10.1109/TEST.2010.5699215</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-1-4244-7206-2</bdi>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:7909084">7909084</a>.</cite>

</li>

<li id="cite_note-5"><a href="#cite_ref-5">^</a> <cite id="CITEREFKarp1972" class="citation book cs1"><a href="Richard_Karp" class="mw-redirect" title="Richard Karp">Karp, Richard M.</a> (1972). <a rel="nofollow" class="external text" href="https://web.archive.org/web/20110629023717/http://www.cs.berkeley.edu/~luca/cs172/karp.pdf">"Reducibility Among Combinatorial Problems"</a> (PDF). In Raymond E. Miller; James W. Thatcher (eds.). Complexity of Computer Computations. New York: Plenum. pp. 85–103. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-306-30707-3</bdi>. Archived from <a rel="nofollow" class="external text" href="http://www.cs.berkeley.edu/~luca/cs172/karp.pdf">the original</a> (PDF) on 2011-06-29. Retrieved 2020-05-07.</cite> Here: p.86

</li>

<li id="cite_note-6"><a href="#cite_ref-6">^</a> <cite id="CITEREFAhoHopcroftUllman1974" class="citation book cs1">Aho, Alfred V.; Hopcroft, John E.; Ullman, Jeffrey D. (1974). The Design and Analysis of Computer Algorithms. Addison-Wesley. p. 403. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-201-00029-6</bdi>.</cite>

</li>

<li id="cite_note-7"><a href="#cite_ref-7">^</a> <cite id="CITEREFMassacciMarraro2000" class="citation journal cs1">Massacci, Fabio; Marraro, Laura (2000-02-01). "Logical Cryptanalysis as a SAT Problem". Journal of Automated Reasoning. 24 (1): 165–203. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1023%2FA%3A1006326723002">10.1023/A:1006326723002</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:3114247">3114247</a>.</cite>

</li>

<li id="cite_note-8"><a href="#cite_ref-8">^</a> <cite id="CITEREFMironovZhang2006" class="citation book cs1">Mironov, Ilya; Zhang, Lintao (2006). <a rel="nofollow" class="external text" href="https://link.springer.com/chapter/10.1007%2F11814948_13">"Applications of SAT Solvers to Cryptanalysis of Hash Functions"</a>. In Biere, Armin; Gomes, Carla P. (eds.). Theory and Applications of Satisfiability Testing - SAT 2006. Lecture Notes in Computer Science. Vol. 4121. Springer. pp. 102–115. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F11814948_13">10.1007/11814948_13</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-540-37207-3</bdi>.</cite>

</li>

<li id="cite_note-9"><a href="#cite_ref-9">^</a> <cite id="CITEREFVizelWeissenbacherMalik2015" class="citation journal cs1">Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "Boolean Satisfiability Solvers and Their Applications in Model Checking". Proceedings of the IEEE. 103 (11): 2021–2035. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FJPROC.2015.2455034">10.1109/JPROC.2015.2455034</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:10190144">10190144</a>.</cite>

</li>

<li id="cite_note-10"><a href="#cite_ref-10">^</a> <cite id="CITEREFCook1971" class="citation book cs1"><a href="Stephen_Cook" title="Stephen Cook">Cook, Stephen A.</a> (1971). <a rel="nofollow" class="external text" href="http://www.cs.toronto.edu/~sacook/homepage/1971.pdf">"The complexity of theorem-proving procedures"</a> (PDF). Proceedings of the third annual ACM symposium on Theory of computing - STOC '71. pp. 151–158. <a href="CiteSeerX_(identifier)" class="mw-redirect" title="CiteSeerX (identifier)">CiteSeerX</a> <a rel="nofollow" class="external text" href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.406.395">10.1.1.406.395</a>. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F800157.805047">10.1145/800157.805047</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:7573663">7573663</a>. <a rel="nofollow" class="external text" href="https://ghostarchive.org/archive/20221009/http://www.cs.toronto.edu/~sacook/homepage/1971.pdf">Archived</a> (PDF) from the original on 2022-10-09.</cite>

</li>

<li id="cite_note-11"><a href="#cite_ref-11">^</a> <cite id="CITEREFLevin1973" class="citation journal cs1"><a href="Leonid_Levin" title="Leonid Levin">Levin, Leonid</a> (1973). "Universal search problems (Russian: Универсальные задачи перебора, Universal'nye perebornye zadachi)". Problems of Information Transmission (Russian: Проблемы передачи информа́ции, Problemy Peredachi Informatsii). 9 (3): 115–116.</cite> <a rel="nofollow" class="external text" href="https://www.mathnet.ru/php/getFT.phtml?jrnid=ppi&paperid=914&volume=9&year=1973&issue=3&fpage=115&what=fullt&option_lang=eng">(pdf)</a> (in Russian), translated into English by <cite id="CITEREFTrakhtenbrot1984" class="citation journal cs1">Trakhtenbrot, B. A. (1984). "A survey of Russian approaches to perebor (brute-force searches) algorithms". Annals of the History of Computing. 6 (4): 384–400. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FMAHC.1984.10036">10.1109/MAHC.1984.10036</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:950581">950581</a>.</cite>

</li>

<li id="cite_note-FOOTNOTEAhoHopcroftUllman1974Theorem_10.4-13"><a href="#cite_ref-FOOTNOTEAhoHopcroftUllman1974Theorem_10.4_13-0">^</a> <a href="#CITEREFAhoHopcroftUllman1974">Aho, Hopcroft & Ullman (1974)</a>, Theorem 10.4.

</li>

<li id="cite_note-FOOTNOTEAhoHopcroftUllman1974Theorem_10.5-16"><a href="#cite_ref-FOOTNOTEAhoHopcroftUllman1974Theorem_10.5_16-0">^</a> <a href="#CITEREFAhoHopcroftUllman1974">Aho, Hopcroft & Ullman (1974)</a>, Theorem 10.5.

</li>

<li id="cite_note-Schoning.1999-17"><a href="#cite_ref-Schoning.1999_17-0">^</a> <cite id="CITEREFSchöning1999" class="citation book cs1">Schöning, Uwe (Oct 1999). <a rel="nofollow" class="external text" href="http://homepages.cwi.nl/~rdewolf/schoning99.pdf">"A probabilistic algorithm for k-SAT and constraint satisfaction problems"</a> (PDF). 40th Annual Symposium on Foundations of Computer Science (Cat. No.99CB37039). pp. 410–414. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FSFFCS.1999.814612">10.1109/SFFCS.1999.814612</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-7695-0409-4</bdi>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:123177576">123177576</a>. <a rel="nofollow" class="external text" href="https://ghostarchive.org/archive/20221009/http://homepages.cwi.nl/~rdewolf/schoning99.pdf">Archived</a> (PDF) from the original on 2022-10-09.</cite>

</li>

<li id="cite_note-18"><a href="#cite_ref-18">^</a> <cite id="CITEREFSelmanMitchellLevesque1996" class="citation journal cs1">Selman, Bart; Mitchell, David; Levesque, Hector (1996). "Generating Hard Satisfiability Problems". Artificial Intelligence. 81 (1–2): 17–29. <a href="CiteSeerX_(identifier)" class="mw-redirect" title="CiteSeerX (identifier)">CiteSeerX</a> <a rel="nofollow" class="external text" href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.7362">10.1.1.37.7362</a>. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1016%2F0004-3702%2895%2900045-3">10.1016/0004-3702(95)00045-3</a>.</cite>

</li>

<li id="cite_note-20"><a href="#cite_ref-20">^</a> <cite id="CITEREFArkinBanikCarmiCitovsky2018" class="citation journal cs1">Arkin, Esther M.; Banik, Aritra; Carmi, Paz; Citovsky, Gui; Katz, Matthew J.; Mitchell, Joseph S. B.; Simakov, Marina (2018-12-11). <a rel="nofollow" class="external text" href="https://doi.org/10.1016%2Fj.dam.2018.05.011">"Selecting and covering colored points"</a>. Discrete Applied Mathematics. 250: 75–86. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1016%2Fj.dam.2018.05.011">10.1016/j.dam.2018.05.011</a>. <a href="ISSN_(identifier)" class="mw-redirect" title="ISSN (identifier)">ISSN</a> <a rel="nofollow" class="external text" href="https://search.worldcat.org/issn/0166-218X">0166-218X</a>.</cite>

</li>

<li id="cite_note-buningkarpinski-21"><a href="#cite_ref-buningkarpinski_21-0">^</a> <cite id="CITEREFBuningKarpinskiFlogel1995" class="citation journal cs1">Buning, H.K.; Karpinski, Marek; Flogel, A. (1995). <a rel="nofollow" class="external text" href="https://doi.org/10.1006%2Finco.1995.1025">"Resolution for Quantified Boolean Formulas"</a>. Information and Computation. 117 (1). Elsevier: 12–18. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1006%2Finco.1995.1025">10.1006/inco.1995.1025</a>.</cite>

</li>

<li id="cite_note-schaefer-22">^ <a href="#cite_ref-schaefer_22-0">a</a> <a href="#cite_ref-schaefer_22-1">b</a> <cite id="CITEREFSchaefer1978" class="citation conference cs1">Schaefer, Thomas J. (1978). <a rel="nofollow" class="external text" href="http://www.ccs.neu.edu/home/lieber/courses/csg260/f06/materials/papers/max-sat/p216-schaefer.pdf">"The complexity of satisfiability problems"</a> (PDF). Proceedings of the 10th Annual ACM Symposium on Theory of Computing. San Diego, California. pp. 216–226. <a href="CiteSeerX_(identifier)" class="mw-redirect" title="CiteSeerX (identifier)">CiteSeerX</a> <a rel="nofollow" class="external text" href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.393.8951">10.1.1.393.8951</a>. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F800133.804350">10.1145/800133.804350</a>.</cite>

</li>

<li id="cite_note-23"><a href="#cite_ref-23">^</a> <cite id="CITEREFMooreMertens2011" class="citation cs2"><a href="Cristopher_Moore" title="Cristopher Moore">Moore, Cristopher</a>; Mertens, Stephan (2011), <a rel="nofollow" class="external text" href="https://books.google.com/books?id=z4zMiZyAE1kC&pg=PA366">The Nature of Computation</a>, Oxford University Press, p. 366, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>9780199233212</bdi></cite>.

</li>

<li id="cite_note-Bryant.German.Velev.1999-24">^ <a href="#cite_ref-Bryant.German.Velev.1999_24-0">a</a> <a href="#cite_ref-Bryant.German.Velev.1999_24-1">b</a> R. E. Bryant, S. M. German, and M. N. Velev, <a rel="nofollow" class="external text" href="http://portal.acm.org/citation.cfm?id=709275">Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions</a>, in Analytic Tableaux and Related Methods, pp. 1–13, 1999.

</li>

<li id="cite_note-25"><a href="#cite_ref-25">^</a> <cite id="CITEREFAkmalWilliams2022" class="citation book cs1">Akmal, Shyan; Williams, Ryan (2022). <a rel="nofollow" class="external text" href="http://web.archive.org/web/20241005152907/https://ieeexplore.ieee.org/document/9719756/">MAJORITY-3SAT (and Related Problems) in Polynomial Time</a>. pp. 1033–1043. <a href="ArXiv_(identifier)" class="mw-redirect" title="ArXiv (identifier)">arXiv</a>:<a rel="nofollow" class="external text" href="https://arxiv.org/abs/2107.02748">2107.02748</a>. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FFOCS52979.2021.00103">10.1109/FOCS52979.2021.00103</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-1-6654-2055-6</bdi>. Archived from <a rel="nofollow" class="external text" href="https://ieeexplore.ieee.org/document/9719756">the original</a> on 2024-10-05. Retrieved 2024-12-25.</cite>

</li>

<li id="cite_note-26"><a href="#cite_ref-26">^</a> <cite id="CITEREFBlassGurevich1982" class="citation journal cs1">Blass, Andreas; Gurevich, Yuri (1982-10-01). <a rel="nofollow" class="external text" href="https://doi.org/10.1016%2FS0019-9958%2882%2990439-9">"On the unique satisfiability problem"</a>. Information and Control. 55 (1): 80–88. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1016%2FS0019-9958%2882%2990439-9">10.1016/S0019-9958(82)90439-9</a>. <a href="Hdl_(identifier)" class="mw-redirect" title="Hdl (identifier)">hdl</a>:<a rel="nofollow" class="external text" href="https://hdl.handle.net/2027.42%2F23842">2027.42/23842</a>. <a href="ISSN_(identifier)" class="mw-redirect" title="ISSN (identifier)">ISSN</a> <a rel="nofollow" class="external text" href="https://search.worldcat.org/issn/0019-9958">0019-9958</a>.</cite>

</li>

<li id="cite_note-27"><a href="#cite_ref-27">^</a> <cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://web.archive.org/web/20190709142353/https://complexityzoo.uwaterloo.ca/Complexity_Zoo:U#US">"Complexity Zoo:U - Complexity Zoo"</a>. complexityzoo.uwaterloo.ca. Archived from <a rel="nofollow" class="external text" href="https://complexityzoo.uwaterloo.ca/Complexity_Zoo:U#US">the original</a> on 2019-07-09. Retrieved 2019-12-05.</cite>

</li>

<li id="cite_note-28"><a href="#cite_ref-28">^</a> <cite id="CITEREFKozen2006" class="citation book cs1">Kozen, Dexter C. (2006). <a rel="nofollow" class="external text" href="https://www.springer.com/gp/book/9781846282973">"Supplementary Lecture F: Unique Satisfiability"</a>. Theory of Computation. Texts in Computer Science. Springer. p. 180. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>9781846282973</bdi>.</cite>

</li>

<li id="cite_note-29"><a href="#cite_ref-29">^</a> <cite id="CITEREFValiantVazirani1986" class="citation journal cs1">Valiant, L.; Vazirani, V. (1986). <a rel="nofollow" class="external text" href="http://www.cs.princeton.edu/courses/archive/fall05/cos528/handouts/NP_is_as.pdf">"NP is as easy as detecting unique solutions"</a> (PDF). Theoretical Computer Science. 47: 85–93. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1016%2F0304-3975%2886%2990135-0">10.1016/0304-3975(86)90135-0</a>.</cite>

</li>

<li id="cite_note-30"><a href="#cite_ref-30">^</a> <cite id="CITEREFBuldasLeninWillemsonCharnamord2017" class="citation book cs1">Buldas, Ahto; Lenin, Aleksandr; Willemson, Jan; Charnamord, Anton (2017). "Simple Infeasibility Certificates for Attack Trees". In Obana, Satoshi; Chida, Koji (eds.). Advances in Information and Computer Security. Lecture Notes in Computer Science. Vol. 10418. Springer International Publishing. pp. 39–55. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-319-64200-0_3">10.1007/978-3-319-64200-0_3</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>9783319642000</bdi>.</cite>

</li>

<li id="cite_note-31"><a href="#cite_ref-31">^</a> <cite id="CITEREFGi-Joon_NamSakallahRutenbar2002" class="citation journal cs1">Gi-Joon Nam; Sakallah, K. A.; Rutenbar, R. A. (2002). <a rel="nofollow" class="external text" href="https://web.archive.org/web/20160315003856/http://cs-rutenbar.web.engr.illinois.edu/wp-content/uploads/2012/10/rutenbar-sattranscad02.pdf">"A new FPGA detailed routing approach via search-based Boolean satisfiability"</a> (PDF). IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 21 (6): 674. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FTCAD.2002.1004311">10.1109/TCAD.2002.1004311</a>. Archived from <a rel="nofollow" class="external text" href="http://cs-rutenbar.web.engr.illinois.edu/wp-content/uploads/2012/10/rutenbar-sattranscad02.pdf">the original</a> (PDF) on 2016-03-15. Retrieved 2015-09-04.</cite>

</li>

<li id="cite_note-32"><a href="#cite_ref-32">^</a> <cite id="CITEREFSelsamLammBünzLiang2019" class="citation arxiv cs1">Selsam, Daniel; Lamm, Matthew; Bünz, Benedikt; Liang, Percy; de Moura, Leonardo; Dill, David L. (11 March 2019). "Learning a SAT Solver from Single-Bit Supervision". <a href="ArXiv_(identifier)" class="mw-redirect" title="ArXiv (identifier)">arXiv</a>:<a rel="nofollow" class="external text" href="https://arxiv.org/abs/1802.03685">1802.03685</a> [<a rel="nofollow" class="external text" href="https://arxiv.org/archive/cs.AI">cs.AI</a>].</cite>

</li>

<li id="cite_note-33"><a href="#cite_ref-33">^</a> <cite class="citation web cs1"><a rel="nofollow" class="external text" href="http://www.satcompetition.org/">"The international SAT Competitions web page"</a>. Retrieved 2007-11-15.</cite>

</li>

</ol></div>

<div class="mw-heading mw-heading2"><h2 id="Sources">Sources</h2></div>

<ul><li>This article includes material from <a rel="nofollow" class="external free" href="https://web.archive.org/web/20070708233347/http://www.sigda.org/newsletter/2006/eNews_061201.html">https://web.archive.org/web/20070708233347/http://www.sigda.org/newsletter/2006/eNews_061201.html</a> by Prof. <a href="Karem_A._Sakallah" title="Karem A. Sakallah">Karem A. Sakallah</a>.</li></ul>

<div class="mw-heading mw-heading2"><h2 id="Further_reading">Further reading</h2></div>

(by date of publication)

/* start https://en.wikipedia.org/ */

.mw-parser-output .refbegin{margin-bottom:0.5em}.mw-parser-output .refbegin-hanging-indents>ul{margin-left:0}.mw-parser-output .refbegin-hanging-indents>ul>li{margin-left:0;padding-left:3.2em;text-indent:-3.2em}.mw-parser-output .refbegin-hanging-indents ul,.mw-parser-output .refbegin-hanging-indents ul li{list-style:none}@media(max-width:720px){.mw-parser-output .refbegin-hanging-indents>ul>li{padding-left:1.6em;text-indent:-1.6em}}.mw-parser-output .refbegin-columns{margin-top:0.3em}.mw-parser-output .refbegin-columns ul{margin-top:0}.mw-parser-output .refbegin-columns li{page-break-inside:avoid;break-inside:avoid-column}@media screen{.mw-parser-output .refbegin{font-size:90%}}

/* end https://en.wikipedia.org/ */

</style><div class="refbegin refbegin-columns references-column-width" style="column-width: 30em">

<ul><li><cite id="CITEREFGareyJohnson1979" class="citation book cs1"><a href="Michael_R._Garey" class="mw-redirect" title="Michael R. Garey">Garey, Michael R.</a>; <a href="David_S._Johnson" title="David S. Johnson">Johnson, David S.</a> (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman. pp. A9.1: LO1–LO7, pp. 259–260. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-7167-1045-5</bdi>.</cite></li>

<li><cite id="CITEREFMarques-SilvaGlass1999" class="citation book cs1">Marques-Silva, J.; Glass, T. (1999). "Combinational equivalence checking using satisfiability and recursive learning". <a rel="nofollow" class="external text" href="http://eprints.soton.ac.uk/265003/1/jpms-date99a.pdf">Design, Automation and Test in Europe Conference and Exhibition, 1999. Proceedings (Cat. No. PR00078)</a> (PDF). p. 145. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FDATE.1999.761110">10.1109/DATE.1999.761110</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-7695-0078-1</bdi>. <a rel="nofollow" class="external text" href="https://ghostarchive.org/archive/20221009/http://eprints.soton.ac.uk/265003/1/jpms-date99a.pdf">Archived</a> (PDF) from the original on 2022-10-09.</cite></li>

<li><cite id="CITEREFClarkeBiereRaimiZhu2001" class="citation journal cs1">Clarke, E.; Biere, A.; Raimi, R.; Zhu, Y. (2001). "Bounded Model Checking Using Satisfiability Solving". Formal Methods in System Design. 19: 7–34. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1023%2FA%3A1011276507260">10.1023/A:1011276507260</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:2484208">2484208</a>.</cite></li>

<li><cite id="CITEREFGiunchigliaTacchella2004" class="citation book cs1">Giunchiglia, E.; Tacchella, A. (2004). Giunchiglia, Enrico; Tacchella, Armando (eds.). Theory and Applications of Satisfiability Testing. Lecture Notes in Computer Science. Vol. 2919. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2Fb95238">10.1007/b95238</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-540-20851-8</bdi>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:31129008">31129008</a>.</cite></li>

<li><cite id="CITEREFBabicBinghamHu2006" class="citation journal cs1 cs1-prop-unfit">Babic, D.; Bingham, J.; Hu, A. J. (2006). <a rel="nofollow" class="external text" href="https://web.archive.org/web/20161023223352/http://www.domagoj-babic.com/uploads/Pubs/TCOM06/tcom06.pdf">"B-Cubing: New Possibilities for Efficient SAT-Solving"</a> (PDF). IEEE Transactions on Computers. 55 (11): 1315. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FTC.2006.175">10.1109/TC.2006.175</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:14819050">14819050</a>. Archived from the original on October 23, 2016.</cite></li>

<li><cite id="CITEREFRodriguezVillagraBaran2007" class="citation book cs1">Rodriguez, C.; Villagra, M.; Baran, B. (2007). <a rel="nofollow" class="external text" href="https://www.cc.pol.una.py/lcca/publicaciones/optimizacion/2007/Asynchronous%20Team%20Algorithms%20for%20Boolean%20Satisfiability.pdf">"Asynchronous team algorithms for Boolean Satisfiability"</a> (PDF). 2007 2nd Bio-Inspired Models of Network, Information and Computing Systems. pp. 66–69. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FBIMNICS.2007.4610083">10.1109/BIMNICS.2007.4610083</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:15185219">15185219</a>.</cite></li>

<li><cite id="CITEREFGomesKautzSabharwalSelman2008" class="citation book cs1"><a href="Carla_Gomes" title="Carla Gomes">Gomes, Carla P.</a>; Kautz, Henry; Sabharwal, Ashish; Selman, Bart (2008). "Satisfiability Solvers". In Harmelen, Frank Van; Lifschitz, Vladimir; Porter, Bruce (eds.). Handbook of knowledge representation. Foundations of Artificial Intelligence. Vol. 3. Elsevier. pp. 89–134. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1016%2FS1574-6526%2807%2903002-7">10.1016/S1574-6526(07)03002-7</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-444-52211-5</bdi>.</cite></li>

<li><cite id="CITEREFVizelWeissenbacherMalik2015" class="citation journal cs1">Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "Boolean Satisfiability Solvers and Their Applications in Model Checking". Proceedings of the IEEE. 103 (11): 2021–2035. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FJPROC.2015.2455034">10.1109/JPROC.2015.2455034</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:10190144">10190144</a>.</cite></li>

<li><cite id="CITEREFKnuth2022" class="citation book cs1 cs1-prop-long-vol"><a href="Donald_Knuth" title="Donald Knuth">Knuth, Donald E.</a> (2022). "Chapter 7.2.2.2: Satifiability". <a href="The_Art_of_Computer_Programming" title="The Art of Computer Programming">The Art of Computer Programming</a>. Vol. 4B: Combinatorial Algorithms, Part 2. Addison-Wesley Professional. pp. 185–369. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-201-03806-4</bdi>.</cite></li></ul>

</div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}

/* end https://en.wikipedia.org/ */

</style><style data-mw-deduplicate="TemplateStyles:r1236075235">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style></div><div role="navigation" class="navbox" aria-labelledby="Logic605" style="padding:3px"><table class="nowraplinks hlist mw-collapsible mw-collapsed navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><style data-mw-deduplicate="TemplateStyles:r1239400231">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div id="Logic605" style="font-size:114%;margin:0 4em"><a href="Logic" title="Logic">Logic</a></div></th></tr><tr><td class="navbox-abovebelow" colspan="2"><div>

<ul><li><a href="History_of_logic" title="History of logic">History</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Major fields</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Logic_in_computer_science" title="Logic in computer science">Computer science</a></li>

<li><a href="Formal_semantics_(natural_language)" title="Formal semantics (natural language)">Formal semantics (natural language)</a></li>

<li><a href="Inference" title="Inference">Inference</a></li>

<li><a href="Philosophy_of_logic" title="Philosophy of logic">Philosophy of logic</a></li>

<li><a href="Formal_proof" title="Formal proof">Proof</a></li>

<li><a href="Semantics_of_logic" title="Semantics of logic">Semantics of logic</a></li>

<li><a href="Syntax_(logic)" title="Syntax (logic)">Syntax</a></li></ul>

</div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%">Logics</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Classical_logic" title="Classical logic">Classical</a></li>

<li><a href="Informal_logic" title="Informal logic">Informal</a>

<ul><li><a href="Critical_thinking" title="Critical thinking">Critical thinking</a></li>

<li><a href="Reason" title="Reason">Reason</a></li></ul></li>

<li><a href="Mathematical_logic" title="Mathematical logic">Mathematical</a></li>

<li><a href="Non-classical_logic" title="Non-classical logic">Non-classical</a></li>

<li><a href="Philosophical_logic" title="Philosophical logic">Philosophical</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Theories</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Argumentation_theory" title="Argumentation theory">Argumentation</a></li>

<li><a href="Metalogic" title="Metalogic">Metalogic</a></li>

<li><a href="Metamathematics" title="Metamathematics">Metamathematics</a></li>

</div></td></tr></tbody></table><div>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Foundations</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Abductive_reasoning" title="Abductive reasoning">Abduction</a></li>

<li><a href="Analytic%E2%80%93synthetic_distinction" title="Analytic–synthetic distinction">Analytic and synthetic propositions</a></li>

<li><a href="Antecedent_(logic)" title="Antecedent (logic)">Antecedent</a></li>

<li><a href="Consequent" title="Consequent">Consequent</a></li>

<li><a href="Contradiction" title="Contradiction">Contradiction</a>

<ul><li><a href="Paradox" title="Paradox">Paradox</a></li>

<li><a href="Antinomy" title="Antinomy">Antinomy</a></li></ul></li>

<li><a href="Deductive_reasoning" title="Deductive reasoning">Deduction</a></li>

<li><a href="Deductive_closure" title="Deductive closure">Deductive closure</a></li>

<li><a href="Definition" title="Definition">Definition</a></li>

<li><a href="Description" title="Description">Description</a></li>

<li><a href="Dichotomy" title="Dichotomy">Dichotomy</a></li>

<li><a href="Logical_consequence" title="Logical consequence">Entailment</a>

<ul><li><a href="Linguistic_entailment" title="Linguistic entailment">Linguistic</a></li></ul></li>

<li><a href="Inductive_reasoning" title="Inductive reasoning">Induction</a></li>

<li><a href="Logical_truth" title="Logical truth">Logical truth</a></li>

<li><a href="Necessity_and_sufficiency" title="Necessity and sufficiency">Necessity and sufficiency</a></li>

<li><a href="Premise" title="Premise">Premise</a></li>

<li><a href="Probability" title="Probability">Probability</a></li>

<li><a href="Proposition" title="Proposition">Proposition</a></li>

<li><a href="Reference" title="Reference">Reference</a></li>

<li><a href="Statement_(logic)" class="mw-redirect" title="Statement (logic)">Statement</a></li>

<li><a href="Substitution_(logic)" title="Substitution (logic)">Substitution</a></li>

<li><a href="Truth" title="Truth">Truth</a></li>

<li><a href="Validity_(logic)" title="Validity (logic)">Validity</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Lists</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="Index_of_logic_articles" class="mw-redirect" title="Index of logic articles">Topics</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="List_of_mathematical_logic_topics" title="List of mathematical logic topics">Mathematical logic</a></li>

<li><a href="List_of_Boolean_algebra_topics" title="List of Boolean algebra topics">Boolean algebra</a></li>

<li><a href="List_of_set_theory_topics" title="List of set theory topics">Set theory</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;">Other</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="List_of_logicians" title="List of logicians">Logicians</a></li>

<li><a href="List_of_rules_of_inference" title="List of rules of inference">Rules of inference</a></li>

<li><a href="List_of_paradoxes" title="List of paradoxes">Paradoxes</a></li>

<li><a href="List_of_fallacies" title="List of fallacies">Fallacies</a></li>

<li><a href="List_of_logic_symbols" title="List of logic symbols">Logic symbols</a></li></ul>

</div></td></tr></tbody></table><div></div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div>

<ul><li> Category</li>

<li> <a href="Outline_of_logic" title="Outline of logic">Outline</a></li>

<li> <a href="Portal%3APhilosophy" title="Portal:Philosophy">Portal</a></li>

<li> WikiProject</li>

<li><a class="external text external" href="https://en.wikipedia.org/w/index.php?title=Special:Recentchangeslinked&target=Template:Logic&hidebots=0">changes</a></li></ul>

</div></td></tr></tbody></table></div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-08-03" href="https://en.wikipedia.org/wiki/?title=Boolean_satisfiability_problem&oldid=1303983242">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>